\begin{tabbing}
$\forall$$w$:World.
\\[0ex]FairFifo
\\[0ex]$\Rightarrow$ (\=$\forall$$e$:E.\+
\\[0ex]state\_after($e$;$\lambda$$e$.w{-}info($w$;$e$);$\lambda$$e$.w{-}pred($w$;$e$);$\lambda$$i$,$x$. s($i$;0).$x$;$\lambda$$i$.
\\[0ex]1of(2of(w{-}machine($w$;$i$)));$\lambda$$e$.val($e$))
\\[0ex]$=$
\\[0ex]($\lambda$$x$.s(loc($e$);time($e$)+1).$x$)
\\[0ex]$\in$ $x$:Id$\rightarrow$vartype(loc($e$);$x$))
\-
\end{tabbing}